Nuprl Lemma : zero_divs_only_zero
2,24
postcript
pdf
a
:
. 0 |
a
a
= 0
latex
Definitions
P
Q
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
divides
wf
origin
a:
. 0 | a 
a = 0 a:. 0 | a a = 0 Qx:A. B(x)
T
x:A. B(x)